D:Dsys, l:IdLnk, i:Id, mss:{m:M(i).Msg| source(mlnk(m)) = i } List.
onlnk(l;mss)  {x:{m:M(i).Msg| source(mlnk(m)) = i }| mlnk(x) = l } List 

latex

Definitions	source(l), IdLnk, Dsys, onlnk(l;mss), Id, M.Msg, M(i), b, , a = b, mlnk(m), x:A. B(x), t  T
Lemmas	mlnk wf d, eq lnk wf, assert wf, filter type, dsys wf, IdLnk wf, Id wf, lsrc wf, d-m wf, ma-msg wf